k, n:, R:(nnProp). (i, j:n. Dec(i R j))  (i, j:n. Dec(i R^k j)) 

latex

Definitions	ij, if b t else f fi, Unit, P  Q, i=j, , b, b, Dec(P), x:A. B(x), x. t(x), R^n, x:A. B(x), {i..j}, , i  j < k, AB, P & Q, A, False, P  Q, x f y, Prop, t  T
Lemmas	rel exp wf, le wf, int seg wf, decidable cand, decidable ex int seg, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, decidable equal int seg, nat wf, decidable wf, nat properties, ge wf